open Syntax
open Hashtbl
open BlockPopulation
open Binding


type proof =  
	| Partial of ty * proof option
	| ProgNode of ty 
	| ForAllElim of proof * ty
	| ImplyElim of proof * proof


type program =  In of int | TypeFunc of program * ty | ObjFunc of program * program


val is_equiv : context->proof->proof->bool
val check_tree : context -> proof -> ty
val exists : context -> proof list -> proof -> bool 
val is_complete : proof->bool
val width : context->ty->ty->int

val string_of_proof : ?output:string -> ?separator:string -> ?line_break:string 
	-> context -> proof -> string
val dotGraphs : context -> proof list -> string
	
val progs_of_proof : ?debug:bool->gene_pool->proof->program list	
val term_of_program : ?debug:bool->gene_pool->proof->program->term
val prog_num : gene_pool->proof list->int
val string_of_program : gene_pool -> (proof * program) -> string 